Inference at * 1 2 
Iof proof for Lemma p-mu-exists:



1. P : 
2. n : 
3. n1:. (n1 < n)  ((P(n1)))  (x: + Top. p-mu(P;x))
4. (P(n))
5. (i:{0..n}. ((P(i))))
  x: + Top. p-mu(P;x) 

latex

 by (InstConcl [inl n ]) 
CollapseTHEN ((Auto) 
CollapseTHEN ((RepUR ``p-mu`` ( 0)) 

CoCollapseTHEN ((Auto) 
CollapseTHEN ((ParallelOp ( -2)) 
CollapseTHEN ((InstConcl [i]) 

CoCollapseTHEN (Auto)))))) 

latex

C.

Definitions	inl x , p-mu(P;x), , Void, A, P  Q, False, x:A. B(x), b, f(a), x:AB(x), {i..j}, , {x:A| B(x)} , i  j < k, P & Q, A  B, x:A. B(x), t  T
Lemmas	assert wf, le wf